\begin{tabbing}
$\forall$$x$, ${\it tg}$:Id, $k$:Knd, $l$:IdLnk, $T$, $A$, $B$:Type.
\\[0ex](rcv($l$,${\it tg}$) $=$ $k$ $\Rightarrow$ $T$ $=$ $B$)
\\[0ex]$\Rightarrow$ (\=$\forall$$f$:($A$$\rightarrow$$B$$\rightarrow$$T$).\+
\\[0ex]@source($l$): $k$(v) sends [${\it tg}$,   $\lambda$$a$,$b$. [$f$($a$,$b$)]($x$, v)] on link $l$   $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@source($l$): $k$(v) sends [${\it tg}$,   $\lambda$$a$,$b$. [$f$($a$,$b$)]($x$, v)] on link $l$   $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]vartype(source($l$);$x$) $\subseteq\rho$ $A$
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ source($l$) $\in$ Id $\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $B$)
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]\& \=sender(${\it e'}$) $=$ $e$ $\in$ E\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex]kind(${\it e''}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ sender(${\it e''}$) $=$ $e$ $\in$ E $\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ E)
\-\\[0ex]\& val(${\it e'}$) $=$ $f$(($x$ when $e$),val($e$)) $\in$ $T$))))
\-\-\-\-\-\-
\end{tabbing}